L:System List, M:System.
(A,BL.A || B)  (BL. interface-compatible(M;B))  interface-compatible(M;(L)) 

latex

Definitions	Feasible(M), P  Q, {T}, x,y. t(x;y), A  B, (x,yL.P(x;y)), xL. P(x), x. t(x), Prop, A || B, l[i], MsgA, Id, {i..j}, i  j < k, AB, P & Q, A, False, P  Q, ||as||, interface-compatible(A;B), (L), Dsys, x:A. B(x), t  T, System
Lemmas	msystem wf, interface-compatible-null, select wf, msga wf, Id wf, m-sys-compatible wf, int seg wf, length wf2, interface-compatible wf, l all wf, pairwise wf, m-sys-join-list-property, interface-compatible-join, l all cons, pairwise-cons, ma-feasible wf